home *** CD-ROM | disk | FTP | other *** search
/ Info-Mac 11 / Info-Mac_XI_Disc_1.cdr_ / Info-Mac XI Disc 1.cdr / Programs / Science & Math / MacEspresso 1.0 / espresso / verify.c < prev   
Encoding:
C/C++ Source or Header  |  1989-02-26  |  4.4 KB  |  186 lines  |  [TEXT/R*ch]
  1. /*
  2.  */
  3.  
  4. #include "espresso.h"
  5.  
  6. /*
  7.  *  verify -- check that all minterms of F are contained in (Fold u Dold)
  8.  *  and that all minterms of Fold are contained in (F u Dold).
  9.  */
  10. bool verify(F, Fold, Dold)
  11. pcover F, Fold, Dold;
  12. {
  13.     pcube p, last, *FD;
  14.     bool verify_error = FALSE;
  15.  
  16.     /* Make sure the function didn't grow too large */
  17.     FD = cube2list(Fold, Dold);
  18.     foreach_set(F, last, p)
  19.     if (! cube_is_covered(FD, p)) {
  20.         printf("some minterm in F is not covered by Fold u Dold\n");
  21.         verify_error = TRUE;
  22.         if (verbose_debug) printf("%s\n", pc1(p)); else break;
  23.     }
  24.     free_cubelist(FD);
  25.  
  26.     /* Make sure minimized function covers the original function */
  27.     FD = cube2list(F, Dold);
  28.     foreach_set(Fold, last, p)
  29.     if (! cube_is_covered(FD, p)) {
  30.         printf("some minterm in Fold is not covered by F u Dold\n");
  31.         verify_error = TRUE;
  32.         if (verbose_debug) printf("%s\n", pc1(p)); else break;
  33.     }
  34.     free_cubelist(FD);
  35.  
  36.     return verify_error;
  37. }
  38.  
  39.  
  40.  
  41. /*
  42.  *  PLA_verify -- verify that two PLA's are identical
  43.  *
  44.  *  If names are given, row and column permutations are done to make
  45.  *  the comparison meaningful.
  46.  *
  47.  */
  48. bool PLA_verify(PLA1, PLA2)
  49. pPLA PLA1, PLA2;
  50. {
  51.     /* Check if both have names given; if so, attempt to permute to
  52.      * match the names
  53.      */
  54.     if (PLA1->label != NULL && PLA1->label[0] != NULL &&
  55.        PLA2->label != NULL && PLA2->label[0] != NULL) {
  56.     PLA_permute(PLA1, PLA2);
  57.     } else {
  58.     fprintf(stderr, "Warning: cannot permute columns without names\n");
  59.     return TRUE;
  60.     }
  61.  
  62.     if (PLA1->F->sf_size != PLA2->F->sf_size) {
  63.     fprintf(stderr, "PLA_verify: PLA's are not the same size\n");
  64.     return TRUE;
  65.     }
  66.  
  67.     return verify(PLA2->F, PLA1->F, PLA1->D);
  68. }
  69.  
  70.  
  71.  
  72. /*
  73.  *  Permute the columns of PLA1 so that they match the order of PLA2
  74.  *  Discard any columns of PLA1 which are not in PLA2
  75.  *  Association is strictly by the names of the columns of the cover.
  76.  */
  77. PLA_permute(PLA1, PLA2)
  78. pPLA PLA1, PLA2;
  79. {
  80.     register int i, j, *permute, npermute;
  81.     register char *labi;
  82.     char **label;
  83.     int strcmp();
  84.  
  85.     /* determine which columns of PLA1 to save, and place these in the list
  86.      * "permute"; the order in this list is the final output order
  87.      */
  88.     npermute = 0;
  89.     permute = ALLOC(int, PLA2->F->sf_size);
  90.     for(i = 0; i < PLA2->F->sf_size; i++) {
  91.     labi = PLA2->label[i];
  92.     for(j = 0; j < PLA1->F->sf_size; j++) {
  93.         if (strcmp(labi, PLA1->label[j]) == 0) {
  94.         permute[npermute++] = j;
  95.         break;
  96.         }
  97.     }
  98.     }
  99.  
  100.     /* permute columns */
  101.     if (PLA1->F != NULL) {
  102.     PLA1->F = sf_permute(PLA1->F, permute, npermute);
  103.     }
  104.     if (PLA1->R != NULL) {
  105.     PLA1->R = sf_permute(PLA1->R, permute, npermute);
  106.     }
  107.     if (PLA1->D != NULL) {
  108.     PLA1->D = sf_permute(PLA1->D, permute, npermute);
  109.     }
  110.  
  111.     /* permute the labels */
  112.     label = ALLOC(char *, cube.size);
  113.     for(i = 0; i < npermute; i++) {
  114.     label[i] = PLA1->label[permute[i]];
  115.     }
  116.     for(i = npermute; i < cube.size; i++) {
  117.     label[i] = NULL;
  118.     }
  119.     FREE(PLA1->label);
  120.     PLA1->label = label;
  121.  
  122.     FREE(permute);
  123. }
  124.  
  125.  
  126.  
  127. /*
  128.  *  check_consistency -- test that the ON-set, OFF-set and DC-set form
  129.  *  a partition of the boolean space.
  130.  */
  131. bool check_consistency(PLA)
  132. pPLA PLA;
  133. {
  134.     bool verify_error = FALSE;
  135.     pcover T;
  136.  
  137.     T = cv_intersect(PLA->F, PLA->D);
  138.     if (T->count == 0)
  139.     printf("ON-SET and DC-SET are disjoint\n");
  140.     else {
  141.     printf("Some minterm(s) belong to both the ON-SET and DC-SET !\n");
  142.     if (verbose_debug)
  143.         cprint(T);
  144.     verify_error = TRUE;
  145.     }
  146.     (void) fflush(stdout);
  147.     free_cover(T);
  148.  
  149.     T = cv_intersect(PLA->F, PLA->R);
  150.     if (T->count == 0)
  151.     printf("ON-SET and OFF-SET are disjoint\n");
  152.     else {
  153.     printf("Some minterm(s) belong to both the ON-SET and OFF-SET !\n");
  154.     if (verbose_debug)
  155.         cprint(T);
  156.     verify_error = TRUE;
  157.     }
  158.     (void) fflush(stdout);
  159.     free_cover(T);
  160.  
  161.     T = cv_intersect(PLA->D, PLA->R);
  162.     if (T->count == 0)
  163.     printf("DC-SET and OFF-SET are disjoint\n");
  164.     else {
  165.     printf("Some minterm(s) belong to both the OFF-SET and DC-SET !\n");
  166.     if (verbose_debug)
  167.         cprint(T);
  168.     verify_error = TRUE;
  169.     }
  170.     (void) fflush(stdout);
  171.     free_cover(T);
  172.  
  173.     if (tautology(cube3list(PLA->F, PLA->D, PLA->R)))
  174.     printf("Union of ON-SET, OFF-SET and DC-SET is the universe\n");
  175.     else {
  176.     T = complement(cube3list(PLA->F, PLA->D, PLA->R));
  177.     printf("There are minterms left unspecified !\n");
  178.     if (verbose_debug)
  179.         cprint(T);
  180.     verify_error = TRUE;
  181.     free_cover(T);
  182.     }
  183.     (void) fflush(stdout);
  184.     return verify_error;
  185. }
  186.